T, T':Type, a:(T List), f, g:(TT').
(x:T. (x  a)  (f(x) = g(x)))  (map(f;a) = map(g;a)  (T' List)) 

latex

Definitions	, t  T, P  Q, x:A. B(x), False, A, A  B, A c B, x:A. B(x), (x  l),
Lemmas	l member wf, nat wf, length wf1, map equal, select wf